\begin{tabbing}
$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:ES, $x$:Id, $e$:E.
\\[0ex]@loc($e$)($x$:$T$)
\\[0ex]$\Rightarrow$ \=($\forall$${\it e'}$:E.\+
\\[0ex](($\uparrow$$x$ changed before $e$) c$\wedge$ ((last change to $x$ before $e$) = ${\it e'}$))
\\[0ex]$\Leftarrow\!\Rightarrow$ \=((${\it e'}$ $<$loc $e$)\+
\\[0ex]\& ($\neg$(($x$ after ${\it e'}$) = ($x$ when ${\it e'}$) $\in$ $T$))
\\[0ex]\& ($\forall$${\it e''}$:E. (${\it e'}$ $<$loc ${\it e''}$) $\Rightarrow$ (${\it e''}$ $<$loc $e$) $\Rightarrow$ (($x$ after ${\it e''}$) = ($x$ after ${\it e'}$) $\in$ $T$))))
\-\-
\end{tabbing}